$\forall$${\it dec}$:(Knd$\rightarrow$Type), ${\it ra}$, ${\it rt}$:(Id$\rightarrow$Id), ${\it rainv}$, ${\it rtinv}$:(Id$\rightarrow$(Id+Unit)).
\\[0ex]($\forall$${\it tg}_{1}$, ${\it tg}_{2}$:Id. ${\it rtinv}$(${\it tg}_{2}$) $=$ inl(${\it tg}_{1}$) $\Rightarrow$ ${\it tg}_{2}$ $=$ ${\it rt}$(${\it tg}_{1}$))
\\[0ex]$\Rightarrow$ ($\forall$$a_{1}$, $a_{2}$:Id. ${\it rainv}$($a_{2}$) $=$ inl($a_{1}$) $\Rightarrow$ $a_{2}$ $=$ ${\it ra}$($a_{1}$))
\\[0ex]$\Rightarrow$ ($\forall$$a$:Action(${\it dec}$). action{-}rename(${\it rainv}$;${\it rtinv}$;$a$) $\in$ Action($\lambda$$k$.${\it dec}$(kind{-}rename(${\it ra}$;${\it rt}$;$k$))))